L:Top List. filter(x.true;L) ~ L 

latex

Definitions	Top, b, xL. P(x), t  T, true, x.A(x), P  Q, x:A. B(x), type List, x:AB(x), s ~ t, (x  l), True
Lemmas	l member wf, filter trivial, btrue wf, top wf